A:Type, eq:EqDecider(A), B:(AType), P:(A), f:x:A fp B(x).
fpf-vals(eq;P;f)  (x:{a:A| P(a) }B(x)) List 

latex

Definitions	Unit, b, A, {T}, Prop, P  Q, P  Q, P & Q, P  Q, strong-subtype(A;B), (x  l), remove-repeats(eq;L), P  Q, b, x. t(x), x(s), , EqDecider(T), x:A. B(x), fpf-vals(eq;P;f), a:A fp B(a), t  T, let x = a in b(x)
Lemmas	deq wf, bool wf, fpf wf, l member wf, remove-repeats wf, strong-subtype-self, strong-subtype-set3, strong-subtype-deq-subtype, cons member, subtype rel list, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert